…process which + exit code 3 + fail-on-missing + failure-details

Same set of #1412/#1413 review fixes applied to the Alloy wrapper:

- Drop unused readdirSync, readFileSync, unlinkSync imports (tsc
  lint failure on #1413)
- Replace /usr/bin/env which shell-out with in-process PATH-scan
  (matches F# AlloyRunnerTests pattern; portable to Windows)
- Exit code 3 for unknown-flag (orthogonal from exit 2 = toolchain
  not ready)
- Treat missing-from-catalogue as failure not skip (catalogue drift
  gate)
- Print per-failure stdout-tail + stderr-tail in --all mode for CI
  triage
- Tightened ExitCode union type per Aaron 2026-05-03 strong-typing
  guidance

Local verification: --check-toolchain OK; InfoTheoreticSharder
passes cleanly; --bad-flag returns exit 3.

…026-05-03) (#1414)

Captures the six author-time disciplines extracted from #1412/#1413
review cycles. Per Aaron 2026-05-03 'any classes to learn to code
better next time via meta learning at PR?' + 'we want to be
strongly typed to a large degree in ts it verifies your
assumptions more at lint time'.

Six classes:

1. Pre-push lint discipline (bun tsc --noEmit catches unused
   imports + typing; CodeQL self-audit for regex injection)
2. Sibling-pattern audit before authoring (when porting F#→TS,
   read F# patterns first)
3. Verify-then-claim applied to comments ('X matches Y' claims
   need grep verification)
4. Exit-code orthogonality (one code = one semantic; document
   contract first; enforce via union types)
5. DX-think on failure paths (failure UX is part of contract;
   print rerun command + stdout-tail)
6. Strong typing as assumption-verifier (union types over
   numbers; brand types over strings; readonly default)

Triggering cases per class documented (each from real #1412/#1413
review threads).

Composes with chat-is-assertion-channel + cache-paths-mutually-
exclusive + the broader verify-then-claim cluster.

MEMORY.md pointer added newest-first.

Carved sentence: 'Apply the review feedback at author-time next
time. Each review thread that closes is a meta-class to
internalize, not just a fix to land.'

…move F# Skip

Reviewer #1415 caught two related issues:
1. Skip removes only CI check for Spine.als (regression after #1413
   landed AlloyRunner.java compile fix; spec was about to be on
   active CI surface)
2. B-0184 'Why P2' was inaccurate — post-#1413 the spec IS running

Aaron 2026-05-03: 'fix them like you normally would'. So instead of
deferring with Skip + P2, fix the spec inline + remove Skip + bump
B-0184 to P1 + close.

Two-part spec fix:

1. Parens around sum-comprehension at line 35:
   (sum b : l.batches | b.size) <= mul[2, cap[l.level, maxCap]]
   Matches comment intent 'total size at level i ≤ 2 * cap(i)'
   (sum-then-compare, not sum-of-Booleans).

2. Replaced check command with fact + run:
   - Original: `check SizeDoublingHolds { SizeDoubling[1] }` —
     asks 'does property hold for ALL bounded instances?' Alloy
     trivially constructs counterexamples by allowing arbitrary
     Int batch sizes (no constraint).
   - Fix: added `fact NonNegativeBatchSizes` (real LSM spines
     have non-negative element counts) + replaced check with
     `run SizeDoublingAdmitsInstance` for constructive existence
     proof. `7 Int` bitwidth bump prevents cap-function overflow.

Local verification: `java -jar alloy.jar exec -f Spine.als`
returns `00. run SizeDoublingAdmitsInstance 0 1/1 SAT` (instance
found). AlloyRunner translates SAT-on-run to OK.

F# Skip removed; Spine [Fact] back on active CI surface.

Backlog row moved P2/ → P1/ to match the bumped priority. Status
flipped to closed. Resolution + 3 discipline lessons appended:

1. Check-vs-run-vs-fact semantic confusion (the substantive
   spec-design lesson)
2. Alloy Int bitwidth must accommodate cap-function range
3. Coverage-loss-is-regression: when a fix becomes part of the
   active CI surface, deferring loses coverage rather than just
   defers it (the reviewer's P2→P1 framing was right)

.gitignore Spine/ (Alloy run-output directory).

Composes with #1413 (the AlloyRunner.java fix that surfaced this)
+ #1414 (PR-review meta-classes memory file — discipline lesson #3
above is a fresh instance of the meta-class).

…t bug surfaced by #1413) (#1415)

* fix+backlog: skip Spine F# Alloy test pending B-0184 spec fix

The pre-#1413 cache-clobber + AlloyRunner.java compile failure was
silently no-op'ing all Alloy tests. Once the cache narrowed (#1404)
and AlloyRunner.java fixed (#1413), CI actually runs Alloy now —
which surfaces the latent Spine.als spec bug at line 35 (Alloy
6.2.0 type-check error: sum-comprehension expects Int but finds
Boolean).

Two parts in this PR:

1. **B-0184 backlog row** filed — captures the spec bug + likely
   intent (sum vs all comprehension confusion) + fix path + the
   silent-skip lineage. P2 since it's pre-existing latent failure
   surfaced post-cleanup.

2. **F# Alloy.Runner.Tests.fs**: add Skip="..." attribute to the
   Spine [Fact] so CI doesn't fail until B-0184 lands. The skip
   message references B-0184 so future-Otto can find the row.

Test result post-fix: 2 passed (InfoTheoreticSharder + jar-
installed), 1 skipped (Spine pending B-0184). Build clean (0/0).

Composes with B-0183 Phase 1 (#1413 surfaced this bug class) +
B-0183 Phase 3 retirement of F# Alloy tests — Spine.als fix needs
to land before TS wrapper retires F# tests so the wrapper passes.

* fix(B-0184): two-part spec fix — parens + check→fact+run + P2→P1 + remove F# Skip

Reviewer #1415 caught two related issues:
1. Skip removes only CI check for Spine.als (regression after #1413
   landed AlloyRunner.java compile fix; spec was about to be on
   active CI surface)
2. B-0184 'Why P2' was inaccurate — post-#1413 the spec IS running

Aaron 2026-05-03: 'fix them like you normally would'. So instead of
deferring with Skip + P2, fix the spec inline + remove Skip + bump
B-0184 to P1 + close.

Two-part spec fix:

1. Parens around sum-comprehension at line 35:
   (sum b : l.batches | b.size) <= mul[2, cap[l.level, maxCap]]
   Matches comment intent 'total size at level i ≤ 2 * cap(i)'
   (sum-then-compare, not sum-of-Booleans).

2. Replaced check command with fact + run:
   - Original: `check SizeDoublingHolds { SizeDoubling[1] }` —
     asks 'does property hold for ALL bounded instances?' Alloy
     trivially constructs counterexamples by allowing arbitrary
     Int batch sizes (no constraint).
   - Fix: added `fact NonNegativeBatchSizes` (real LSM spines
     have non-negative element counts) + replaced check with
     `run SizeDoublingAdmitsInstance` for constructive existence
     proof. `7 Int` bitwidth bump prevents cap-function overflow.

Local verification: `java -jar alloy.jar exec -f Spine.als`
returns `00. run SizeDoublingAdmitsInstance 0 1/1 SAT` (instance
found). AlloyRunner translates SAT-on-run to OK.

F# Skip removed; Spine [Fact] back on active CI surface.

Backlog row moved P2/ → P1/ to match the bumped priority. Status
flipped to closed. Resolution + 3 discipline lessons appended:

1. Check-vs-run-vs-fact semantic confusion (the substantive
   spec-design lesson)
2. Alloy Int bitwidth must accommodate cap-function range
3. Coverage-loss-is-regression: when a fix becomes part of the
   active CI surface, deferring loses coverage rather than just
   defers it (the reviewer's P2→P1 framing was right)

.gitignore Spine/ (Alloy run-output directory).

Composes with #1413 (the AlloyRunner.java fix that surfaced this)
+ #1414 (PR-review meta-classes memory file — discipline lesson #3
above is a fresh instance of the meta-class).

Backlog generator drift catch from PR #1416 — `bun tools/backlog/generate-index.ts`
needs to be re-run after moving a row between priority directories.
Same author-time class as B-0184 P2->P1 move (same #1413/#1415 cycle).

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Backlog generator drift catch from PR #1416 — `bun tools/backlog/generate-index.ts`
needs to be re-run after moving a row between priority directories.
Same author-time class as B-0184 P2->P1 move (same #1413/#1415 cycle).

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

… -> A: 4 of 4 deferred specs in CI) (#1416)

* fix(tla): SpineMergeInvariants counterexample (B-0181 P2->P1 closed)

Cascade(i) was under-specified: only required levels[i] >= Cap(i), no
constraint on level i+1. TLC found a 16-step trace where Cascade(0)
fires 5 times in a row, accumulating level 1 to 10 > 2*Cap(1) = 8 even
though Cascade(1) was enabled the whole time.

Fix mirrors the synchronous cascade chain in BalancedSpine.fs: add
levels[i+1] + levels[i] <= 2 * Cap(i+1) precondition so a level can't
dump while its downstream is at the cap-overshoot boundary. Added
WF_vars(Cascade(i)) for liveness. Added StateBound + PendingBound
constraints with bounded constants (MaxLevel=2 / MaxBatchSize=1) so
TLC's BFS terminates: 400 distinct states, depth 45, both InvCap and
InvMass hold.

Wired CI registration: [<Fact>] TLC validates SpineMergeInvariants in
tests/Tests.FSharp/Formal/Tlc.Runner.Tests.fs. Closes B1 -> A in the
math-proofs honest assessment matrix (4 of 4 deferred TLA+ specs now
in CI). Promoted P2 -> P1 because same author-time class as B-0184
(Alloy Spine.als under-specified pred): under-specified action
preconditions across two different formal-verification tools.

.gitignore: covered both run-from-tools/tla and run-from-tools/tla/specs
TLC state directories + TTrace files.

Memory: feedback_under_specified_action_preconditions_recurring_class_in_formal_specs_aaron_2026_05_03.md
captures the recurring class with author-time precondition-audit
discipline.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

* docs(backlog): regenerate index after B-0181 P2->P1 move

Backlog generator drift catch from PR #1416 — `bun tools/backlog/generate-index.ts`
needs to be re-run after moving a row between priority directories.
Same author-time class as B-0184 P2->P1 move (same #1413/#1415 cycle).

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

* review(B-0181): address Copilot feedback on #1416

Two of three Copilot comments addressed (third — BACKLOG.md regen — was
already addressed by 9350572 / commit-2 of this branch):

1. Updated StateBound's comment in SpineMergeInvariants.tla to reflect
   actual model constraints (PendingBound also active in cfg) — drops
   the misleading "16-slot pendingIn = 30" calculation that was based
   on Accept's loose internal bound rather than the effective cfg
   constraints. Both bounds now jointly justified.

2. Replaced the closed row's "Investigation needed" section with
   "Investigation summary (resolved)" — past-tense triage of the three
   failure classes plus which one applied (none of spec-incorrect /
   invariant-over-spec / real-BalancedSpine-bug; the actual class was
   under-specified action precondition).

TLC still clean: 400 distinct states, depth 45, both InvCap and
InvMass hold.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>

… shard (#1418)

* hygiene(tick-history): 2026-05-03T15:12Z session-summary tick

B-0181 SpineMergeInvariants closure (#1416 merged) + B-0183 Phase 1
sibling Alloy TS wrapper landed (#1413 merged after rebase) +
Stryker B3 workflow opened (#1417). Math-proofs assessment matrix:
B1 -> A fully closed (4/4 deferred TLA+ specs in CI); B3 in-flight
closure now pending.

Discipline lesson encoded: under-specified-action-preconditions as
recurring class across formal-verification tools (TLA+ + Alloy).
Author-time precondition-audit is the structural fix.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

* fix(tick-shard): escape glob ** to satisfy markdownlint MD037

src/Core/** + tests/Tests.FSharp/** rendered the ** as bold-end with
a space, tripping MD037 no-space-in-emphasis. Backtick-quote the path
patterns to suppress markdown emphasis interpretation.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

* review(tick-shard): use cron-id (a2e2cc3a) in col3 per shard schema

Reviewer caught: 3rd column documented as cron sentinel/id, not action
summary. Move "post-1330Z session compaction recovery + B-0181 closure"
into the body column where it belongs.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>